package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.TreeSet;

import edu.uic.cs.cs582.misc.Assert;
import edu.uic.cs.cs582.misc.GeneralException;
import edu.uic.cs.cs582.process.impl.IntArrayComparator;

class MiddleVariableExpression extends AbstractVariablesOperations
{
	private static final IntArrayComparator COMPARATOR = new IntArrayComparator();

	private static class SortedAddArrayList extends ArrayList<int[]>
	{
		private static final long serialVersionUID = 4289534836450229881L;

		public SortedAddArrayList(int initialCapacity)
		{
			super(initialCapacity);
		}

		@Override
		public boolean add(int[] e)
		{
			Arrays.sort(e);
			return super.add(e);
		}
	}

	private List<int[]> expressionInDnf;
	private List<int[]> notExpressionInDnf;

	//	private List<int[]> expressionInCnf;
	//	private List<int[]> notExpressionInCnf;

	public MiddleVariableExpression(int[]... clauses)
	{
		super(null);

		// sort ////////////////////////////////////////////////////////////////
		for (int[] clause : clauses)
		{
			Arrays.sort(clause);
		}
		expressionInDnf = Arrays.asList(clauses);
		Collections.sort(expressionInDnf, COMPARATOR);
	}

	private void initializeNotExpression()
	{
		switch (expressionInDnf.size())
		{
			case 1:
				initializeNotExpression(expressionInDnf.get(0));
				break;
			case 2:
				initializeNotExpression(expressionInDnf.get(0),
						expressionInDnf.get(1));
				break;
			case 3:
				initializeNotExpression(expressionInDnf.get(0),
						expressionInDnf.get(1), expressionInDnf.get(2));
				break;
			case 4:
				initializeNotExpression(expressionInDnf.get(0),
						expressionInDnf.get(1), expressionInDnf.get(2),
						expressionInDnf.get(3));
				break;
			default:
				throw new GeneralException("Only support 4 clauses in DNF. ");

		}

		Collections.sort(notExpressionInDnf, COMPARATOR);
	}

	// not (a and b) -> (not a) or (not b)
	private void initializeNotExpression(int[] clause)
	{
		Assert.isTrue(clause.length == 2);

		notExpressionInDnf = new SortedAddArrayList(2);
		for (int variable : clause)
		{
			notExpressionInDnf.add(new int[] { not(variable) });
		}
	}

	// not ((a and (not b)) or ((not a) and b)) -> (a and b) or ((not a) and (not b))
	private void initializeNotExpression(int[] clause1, int[] clause2)
	{
		Assert.isTrue(clause1.length == 2);
		Assert.isTrue(clause2.length == 2);

		int a = Math.abs(clause1[0]);
		int b = Math.abs(clause1[1]);

		int _a = Math.abs(clause2[0]);
		int _b = Math.abs(clause2[1]);
		Assert.isTrue((a == _a && b == _b) || (a == _b && b == _a));
		////////////////////////////////////////////////////////////////////////

		notExpressionInDnf = new SortedAddArrayList(2);
		notExpressionInDnf.add(new int[] { a, b });
		notExpressionInDnf.add(new int[] { not(a), not(b) });
	}

	private void initializeNotExpression(int[] clause1, int[] clause2,
			int[] clause3)
	{
		int[][] allClauses = new int[][] { clause1, clause2, clause3 };
		TreeSet<Integer> allVariables = new TreeSet<Integer>();
		for (int[] clause : allClauses)
		{
			Assert.isTrue(clause.length == 2);
			for (int variable : clause)
			{
				Assert.isTrue(variable > 0);
				allVariables.add(variable);
			}
		}
		Assert.isTrue(allVariables.size() == 3);
		int a = allVariables.pollFirst();
		int b = allVariables.pollFirst();
		int c = allVariables.pollFirst();
		////////////////////////////////////////////////////////////////////////

		notExpressionInDnf = new SortedAddArrayList(3);
		notExpressionInDnf.add(new int[] { not(b), not(a) });
		notExpressionInDnf.add(new int[] { not(c), not(a) });
		notExpressionInDnf.add(new int[] { not(c), not(b) });

	}

	private void initializeNotExpression(int[] clause1, int[] clause2,
			int[] clause3, int[] clause4)
	{
		int[][] allClauses = new int[][] { clause1, clause2, clause3, clause4 };
		TreeSet<Integer> allVariables = new TreeSet<Integer>();
		for (int[] clause : allClauses)
		{
			Assert.isTrue(clause.length == 3);
			for (int variable : clause)
			{
				allVariables.add(Math.abs(variable));
			}
		}
		Assert.isTrue(allVariables.size() == 3);
		int a = allVariables.pollFirst();
		int b = allVariables.pollFirst();
		int c = allVariables.pollFirst();
		////////////////////////////////////////////////////////////////////////

		notExpressionInDnf = new SortedAddArrayList(4);

		notExpressionInDnf.add(new int[] { not(c), not(b), not(a) });
		notExpressionInDnf.add(new int[] { not(c), a, b });
		notExpressionInDnf.add(new int[] { not(b), a, c });
		notExpressionInDnf.add(new int[] { not(a), b, c });
	}

	public List<int[]> getExpressionInDnf()
	{
		return expressionInDnf;
	}

	public List<int[]> getNotExpressionInDnf()
	{
		if (notExpressionInDnf == null)
		{
			initializeNotExpression();
		}

		return notExpressionInDnf;
	}

	//	public List<int[]> getExpressionInCnf()
	//	{
	//		if (expressionInCnf == null)
	//		{
	//			expressionInCnf = convertDnfToCnf(getExpressionInDnf());
	//		}
	//
	//		return expressionInCnf;
	//	}
	//
	//	public List<int[]> getNotExpressionInCnf()
	//	{
	//		if (notExpressionInCnf == null)
	//		{
	//			notExpressionInCnf = convertDnfToCnf(getNotExpressionInDnf());
	//		}
	//
	//		return notExpressionInCnf;
	//	}
}